Nuprl Definition : order 13,42
compound
Order(T;x,y.R(x;y)) == Refl(T;x,y.R(x;y)) & Trans(T;x,y.R(x;y)) & AntiSym(T;x,y.R(x;y)) 
latex

Uprel 1, rel 1
Wellformedness Lemmasorder wf, order wf
DefinitionsRefl(T;x,y.E(x;y)), P & Q, Trans(T;x,y.E(x;y)), AntiSym(T;x,y.R(x;y))
FDL editor aliasesorder

origin